a, b:, p:FinProbSpace, F, G:(Outcome).
weighted-sum(p;x.(a * (F(x))) + (b * (G(x))))
=
((a * weighted-sum(p;F)) + (b * weighted-sum(p;G)))
  

latex

Definitions	Void, t  T, x:A.B(x), Top, , type List, x:AB(x), x:A. B(x), S  T, FinProbSpace, Outcome, ||as||, #$n, {i..j}, s = t, , {x:A| B(x)} , suptype(S; T)
Lemmas	weighted-sum-linear, finite-prob-space wf, length wf nat, nat wf, p-outcome wf, int seg wf, length wf1, top wf, rationals wf